T:Type, L:T List, P:(TT). count(x < y in L | P(x,y))   

latex

Definitions	b, b, Prop, P  Q, Unit, x. t(x), sum(f(x) | x < k), sum(f(x;y) | x < n; y < m), x:A. B(x), ij, ||as||, t  T, , P  Q, False, A, AB, P & Q, i  j < k, {i..j}, , l[i], x(s1,s2), i<j, p  q, if b t else f fi, x,y. t(x;y), count(x < y in L | P(x;y))
Lemmas	double sum wf, ifthenelse wf, band wf, lt int wf, select wf, int seg wf, le wf, length wf1, bool wf, non neg length, sum wf, non neg sum, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, assert wf